package main;

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Date;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Vector;

import main.Instance.Weight;

import utils.IOUtils;
import utils.Pair;
import utils.StreamGobbler;

public class Main {

	public static String COMMON_FILE_NAME = "Lefel_Zilberman/graph_";
	
	public static void main(String[] args) throws IOException{
		new File("./Lefel_Zilberman").mkdir();
		String instanceFile = "instances/graph_10.instance";
		if (args.length > 0){
			instanceFile = args[0];
		}
		File logFile = new File("Lefel_Zilberman/satLogger.csv");
		FileWriter fw = new FileWriter(logFile);
		fw.write("Instance#,#Nodes,EncodingTime,#Clause,#Variable,SATSolvingTime,SolutionSize,OptimalSize" + IOUtils.lineSeperator);
		fw.flush();
		run(instanceFile, fw);
		fw.close();
	}
	
	public static void run(String instanceFile, FileWriter fw) throws IOException{

		int instanceNumber = Integer.parseInt(instanceFile.substring(instanceFile.lastIndexOf("_")+1, instanceFile.indexOf(".")));
		
		Instance instance = IOUtils.loadInstanceFile(instanceFile);
		System.out.println("Problem instance file loaded");
		
		boolean connected = Verifier.isConnected(instance.getGraph());
		if (!connected){
			String solFileName = COMMON_FILE_NAME + instanceNumber +".sol";
			IOUtils.generateNoSolFile(solFileName);
			System.out.println("Graph not connected!!");
			return;
		}
		
		// Initialize mapping object
		LiteralAlocatorAndMap map = new LiteralAlocatorAndMap(instance.getNumOfVertices());
		Date startEncoding = new Date();
		Vector<int[]> cnf = generateClauses(map,instance);
		int[] sumBits = map.getSumBits();
		Date endEncoding = new Date();
		if (fw != null ){
			fw.append(instanceNumber + "," + instance.getNumOfVertices() + ",");
			fw.append(((endEncoding.getTime()-startEncoding.getTime()) /(double) 1000) +"," + cnf.size() + ","  );
			fw.append(map.lastLiteral() +",");
			fw.flush();
		}
		// Generate script file
		String scriptFileName = COMMON_FILE_NAME + instanceNumber + ".script";
		IOUtils.generateScriptFile(scriptFileName, cnf, sumBits);
		
		try {
			// Apply SCryptoMiniSat 
			String satFilePath = COMMON_FILE_NAME + instanceNumber + ".sat";
			Date start = new Date();
			Process pr = execut("lib/SCryptoMinisatWin64.exe", COMMON_FILE_NAME + instanceNumber + ".script",  satFilePath);
			int err = pr.waitFor();
			Date end = new Date();
			
			long satSolvingTime = end.getTime()-start.getTime();
			Solution sol = Decoder.getSolution(satFilePath, map);
			
			System.out.println("Time to solve instance #" + instanceNumber + " -> " + satSolvingTime);
			if (fw != null ) {
				fw.append( (satSolvingTime/(double) 1000) + ",");
				fw.append(sol.getNumOfStrong() + ",");
				fw.append(instance.getOptimalSolution() + IOUtils.lineSeperator );
				fw.flush();
			}
				
			
			boolean verified = Verifier.verify(sol.getNodes(), instance.getEdges());
			String solFileName = COMMON_FILE_NAME + instanceNumber +".sol";
			IOUtils.generateSolFile(solFileName, sol);
			
			if (verified){
				
				String dotFilePath = COMMON_FILE_NAME + instanceNumber +".dot";
				IOUtils.generateDotFile(dotFilePath,instance.getEdges(),sol);
				try{
					//generating png file - visualizing the solution
					pr = execut("dot","-Tpng","-O", new File(dotFilePath).getAbsolutePath());
					err = pr.waitFor();
					
					//open the png file
					pr = execut("cmd.exe","/c","start",new File(dotFilePath + ".png").getAbsolutePath());
					
				}catch(Exception e){
					e.printStackTrace();
				}
				
				
			}
			else{
				System.out.println("ERROR IN SOLUTION!!");
			}
		} catch (Exception e) {
			e.printStackTrace();
		}
	}

	private static Vector<int[]> generateClauses(LiteralAlocatorAndMap map, Instance instance) {
		Vector<int[]> cnf = map.generateNodesLits();
		int zeroLit = map.getZeroLit();
		cnf.add(new int[]{-zeroLit});
		Map<Pair<Integer, Integer>, Weight> edges = instance.getEdges();
		for (Entry<Pair<Integer, Integer>, Weight> e : edges.entrySet()) {
			Weight weight = e.getValue();
			int newLit = map.newEdge(e.getKey().first, e.getKey().second, weight);
			cnf.add(new int[]{newLit});
			weight = weight.equals(Weight.SHORT)?Weight.LONG:Weight.SHORT;
			newLit = map.newEdge(e.getKey().first, e.getKey().second, weight);
			cnf.add(new int[]{-newLit});
		}
		for (int length = 1; length <= instance.getNumOfVertices()-1; length++){
			for (int i=1; i<=instance.getNumOfVertices(); i++){
				for (int j=1; j<=instance.getNumOfVertices(); j++){
					if (i!=j){
						Pair<Integer, Integer> ij = new Pair<Integer, Integer>(i, j);
						int p_ij = map.getPathLiteral(ij,length);
						if (length == 1) {
							int i_strong = map.getStrongNodeLit(i);
							if (map.isEdge(i, j)){
								int ij_long = map.getEdgeLiteral(i, j, Weight.LONG);
								int ij_short = map.getEdgeLiteral(i, j, Weight.SHORT);
								cnf.add(new int[]{p_ij,-ij_short});
								cnf.add(new int[]{p_ij, ij_short, -ij_long, -i_strong});
								cnf.add(new int[]{-p_ij, ij_short, -ij_long, i_strong});
								cnf.add(new int[]{-p_ij, ij_short, ij_long, -i_strong});
							}else{
								cnf.add(new int[]{-p_ij});
							}
						}else{
							int t1 = map.getPathLiteral(ij,length);
							for (int k=1; k <= map.getNumOfVertices(); k++){
								if (k != i && k != j){
									int p_ik = map.getPathLiteral(new Pair<Integer, Integer>(i, k), 1);
									int p_kj = map.getPathLiteral(new Pair<Integer, Integer>(k, j), length-1);
									int t2 = map.newOther("");
									cnf.add(new int[]{-t2, t1});
									cnf.add(new int[]{p_ik, p_kj, t2, -t1});
									cnf.add(new int[]{p_ik, -p_kj, t2, -t1});
									cnf.add(new int[]{-p_ik, p_kj, t2, -t1});
									cnf.add(new int[]{-p_ik, -p_kj, t1});
									t1 = t2;
								}
							}
							cnf.add(new int[]{-t1});
						}
					}
				}
			}
		}
		for (int i=1; i<=instance.getNumOfVertices(); i++){
			for (int j=1; j<=instance.getNumOfVertices(); j++){
				if (i!=j){
					int[] lits = new int[instance.getNumOfVertices()-1];
					for (int length = 1; length <= instance.getNumOfVertices()-1; length++){
						Pair<Integer, Integer> ij = new Pair<Integer, Integer>(i, j);
						int p_ij = map.getPathLiteral(ij,length);
						lits[length-1] = p_ij;
					}
					cnf.addAll(Encoder.atLeastOne(lits));
				}
			}
		}
		//Add sums cnf
		int[] strongNodesLiterals = map.getStrongNodeLits();
		int[] strongNodesLitsCopy = new int[strongNodesLiterals.length];
		for (int i = 0; i < strongNodesLiterals.length; i++){
			strongNodesLitsCopy[i] = strongNodesLiterals[i];
		}
		
		Vector<int[]> sumCnf = new Vector<int[]>();
		int[] sumBits = Encoder.fullAdder(strongNodesLitsCopy, map, sumCnf);
		map.setSumBits(sumBits);
		cnf.addAll(sumCnf);
		return cnf;
	}

	private static Process execut(String ... cmd) throws IOException {
		ProcessBuilder pb;
		Process pr;
		pb = new ProcessBuilder(cmd);
		pb.redirectErrorStream(true);
		pr = pb.start();
		StreamGobbler.gobble(pr.getInputStream());
		return pr;
	}
	
	
}
